An overview of the liquid tensor experiment

Abstract: In December 2020, Peter Scholze proposed a challenge to formally verify a theorem he and Dustin Clausen proved about the real numbers in the context of condensed mathematics, saying it might be his "most important theorem to date." I was part of the group who took on this challenge, using the Lean3 interactive theorem prover and its formally verified mathematics library `mathlib`. We completed the challenge in July 2022. In this talk, I will give a broad overview of condensed/liquid mathematics and the corresponding formalization in Lean. No background in condensed mathematics or interactive theorem provers will be necessary for this talk.

algebraic geometrynumber theory

Audience: researchers in the topic

SFU NT-AG seminar

Series comments: The Number Theory and Algebraic Geometry (NT-AG) seminar is a research seminar dedicated to topics related to number theory and algebraic geometry hosted by the NT-AG group (Nils Bruin, Imin Chen, Stephen Choi, Katrina Honigs, Nathan Ilten, Marni Mishna).

We acknowledge the support of PIMS, NSERC, and SFU.

For Fall 2025, the organizers are Katrina Honigs and Peter McDonald.

We normally meet in-person in the indicated room. For online editions, we use Zoom and distribute the link through the mailing list. If you wish to be put on the mailing list, please subscribe to ntag-external using lists.sfu.ca